2019-01-04

Кодировка Изоморфизмами

Специально для канала Формальная Философия. В статье не рассматривается ничего сложнее чем encode-decode XML <-> JSON вместе с правилами enc dec = id и dec enc = id. Просто вместо переменных XML/JSON мы рассматриваем несколько конкретных типов: Iso, Equiv, Pi, Interval. Другими словами, мы будем кодировать эти типы и транспорты между ними с помощью изоморфизмов.

Вступление

Как вы знаете все индуктивные типы (Nat, List и т.д.) могут быть представлены в Чёрч-кодировке которая есть упаковка категорной модели. Идея кодирования следующая, раз мы работаем в теории категорий, то всё сущности мы рассматриваем как объекты и связи между ними (везде одно и то же). Значит и индуктивные типы мы раскладываем в это же, т.е. другими словами мы строим категорную модель конкретных индуктивных инстансов data, или как говорят мы строим категории F-алгебр:


 natOb: U
   = (X: U)
   * (zero: X)
   * (succ: X -> X)
   * unit

 natHom (x1 x2: natOb): U
   = (map: x1.1 -> x2.1)
   * (mapZero: Path x2.1 (map (x1.2.1)) (x2.2.1))
   * (mapSucc: (x: x1.1) -> Path x2.1 (map (x1.2.2.1 x)) (x2.2.2.1 (map x)))
   * unit

 isHomotopyInitialNat (I: natOb): U
   = (C:  natOb)
   * (x:  natHom I C)
   * ((y: natHom I C) -> Path (natHom I C) x y)

Здесь у нас unit-терминейтед record — это что-то типа null-терминейтед стринг. Я думаю идея понятна. Если взять лимит в этой категории получится штука изоморфная черч-кодировке. В HoTT это можно увидеть в параграфе Nat-алгебр (5.4.1) и Nat-гомоморфизмов (5.4.2). Полная кодировка должна включать не только зависимый элиминатор, через который уже выражается рекурсор и кейс анализ, но и правила связывающие фьюжин intro-elim двумя правилами beta и eta которые называются ещё ректракт и секция (enc dec = id, dec enc = id).

Постановка задачи

В этой статье мы покажем, что, во-первых, интернализация MLTT в сущности есть кодировкой изоморфизмами, и, во-вторых, покажем, что в кодировке Пи у нас функция равна своей аппликации (да да, вам не послышалось).

Ну, я думаю не нужно доказывать или показывать, что всё в MLTT есть тип, или всё в мире есть феномен. А раз так, то мы можем построить категорию этих объектов и морфизмов между ними (это у математиков что-то типа если есть гора, то на неё нужно взобраться, или как я называю в любой непонятной ситуации строй категорию). Т.е. тоеретически возможно засунуть любой тип в сигнатуру изоморфизма:


 isIso (XML JSON: U): U        -- form
   = (f: XML -> JSON)          -- intro
   * (g: JSON -> XML)          -- elim
   * (s: section XML JSON f g) -- beta
   * (   retract XML JSON f g) -- eta

 section (A B:U) (f:A->B) (g:B->A): U
   = (b:B) -> Path B (f(g(b))) b

 retract (A B:U) (f:A->B) (g:B->A): U
   = (a:A) -> Path A (g(f(a))) a

Давайте попробуем это сделать для сложных типов, чтобы доказать первую часть задачи, а потом попробуем закодировать самый базовый Пи-тип на котором строится вся теория MLTT, и докажем вторую часть задания.

Аксиома Унивалентности

Она не золотой грааль, а обычнейший тип, а значит для нее существует 5 правил теории типов Мартина-Лёфа. В сущности, чтобы не лукавить, надо сказать, что унивалентность вшивается в тайпчекеры обычно. В cubicaltt intro-правило типовой унивалентности называется Glue.


 univ_Formation (A B: U)
   : U = equiv A B -> Path U A B -- Formation
 equivToPath (A B: U)
   : univ_Formation A B -- Intro
 pathToEquiv (A B: U) (p: Path U A B)
   : equiv A B -- Elim
 eqToEq (A B : U) (p : Path U A B)
   : Path (Path U A B) (equivToPath A B
                       (pathToEquiv A B p)) p -- Beta
 idToPath (A B: U) (w: equiv A B)
   : Path (equiv A B)  (pathToEquiv A B
                       (equivToPath A B w)) w -- Eta

Превращаем аксиому унивалентности в енкодер-декодер или изоморфизм:


 UnivType (A B: U): isIso (equiv A B) (Path U A B)
   = (equivToPath A B, pathToEquiv A B,eqToEq A B,idToPath A B)

Неплохо, поехали дальше.

Изоморфизм Изоморфизма

Так как фибрационная эквивалентность есть одним из видов равенства и аксиома унивелентности это в сущности часть конструкции которая связывает фьюжин типов фибрационной эквивалентности Equiv и типа Path встроенного в кубический тайпчекер, то можно построить точно такой же изоморфизм между Path и типом Iso, который так же является одним из видов равенства, простой и поняный всем программистам encode/decode.


 iso_Form (A B: U)
   : U = isIso A B -> Path U A B
 iso_Intro (A B: U)
   : iso_Form A B
 iso_Elim (A B: U)
   : Path U A B -> isIso A B
 iso_Comp (A B : U) (p : Path U A B)
   : Path (Path U A B) (iso_Intro A B (iso_Elim A B p)) p
 iso_Uniq (A B : U) (p: isIso A B)
   : Path (isIso A B) (iso_Elim A B (iso_Intro A B p)) p

Заметьте как мы циклически встраиваемся в нижний уровень подсвовывая в сами изоморфизм сигнатуру с изоморфизмом


 IsoPathType (A B: U): isIso (isIso A B) (Path U A B)
   = (iso_Intro A B,iso_Elim A B,iso_Comp A B,iso_Uniq A B)

Пи-тип

Теперь давайте перейдем к самому простому и самому загадночному изоморфизму изоморфизму Пи-типов. Вспомним категорные догматы: чтобы закодировать что-то, нам надо построить категорию эндоморфизмов этого. В нашем случае, так как мы отложили учебник по теоркату и вышиваем на XML <-> JSON сигнатурах, мы просто строим изоморфизм между Пи и Пи:


 PiType (A: U) (B: A -> U): isIso (Pi A B) (Pi A B)
   = (app A B,lam A B,Pi_Beta A B,Pi_Eta A B)


 Pi (A: U) (B: A -> U)
   : U = (x:A) -> B(x)
 lam (A: U) (B: A -> U) (b: Pi A B)
   : Pi A B = \(x: A) -> b x
 app (A: U) (B: A -> U) (f: Pi A B) (a: A)
   : B a = f a
 Pi_Beta (A: U) (B: A -> U) (f: Pi A B)
   : Path (Pi A B) (\(x:A) -> f x) f
 Pi_Eta (A: U) (B: A -> U) (f: Pi A B)
   : Path (Pi A B) f (\(x:A) -> f x)

Как видно мы тут немного подхачили, но вполне законно так как мы просто перенесли a : A из телескопа параметров в правую часть результата и протащили в путь: Path (B a) -> Path (Pi A B).


 beta_classic (A:U)(B:A->U)(f: Pi A B) (a:A) : Path (B a) ((lambda A B f) a) (f a)
 Pi_Beta      (A:U)(B:A->U)(f: Pi A B)    : Path (Pi A B) (\(x:A) -> f x) f

Теперь докажем вторую задачу и главный номер представления (то, что функция равна своей аппликации, ну бредятина же на звук!):


 PiType (A: U) (B: A -> U): isIso (Pi A B) (Pi A B)
   = (lam A B,lam A B,Pi_Beta A B,Pi_Eta A B)
   = (app A B,lam A B,Pi_Beta A B,Pi_Eta A B)
   = (app A B,app A B,Pi_Eta A B,Pi_Eta A B)

Любой из этих вариантов чекается!


 Checking: PiType
 File loaded.
 >

На самом деле, такие тавтологии рождаются потому, что мы в isIso поставили равные типы, до этого в примерах мы делали транспорты из крайних точек пути, тут же у нас петля. Но, тем не менее, этот терм PiType в разных инкарнация вы можете встретить в любой статье про лямбда исчисление, так как он является вычислительной семантикой зависимого лямбда исчисления (для примера классическая запись в виде терма PTS):


 PTS (A: U): U
   = (Pi_Former:   (A -> U) -> U)
   * (Pi_Intro: (B: A -> U) -> Pi A B -> Pi A B)
   * (Pi_Elim:  (B: A -> U) -> Pi A B -> Pi A B)
   * (Pi_Comp1: (B: A -> U) (a: A) (f: Pi A B)
  -> Equ (B a) (Pi_Elim B (Pi_Intro B f) a) (f a))
   * (Pi_Comp2: (B: A -> U) (a: A) (f: Pi A B)
  -> Equ (Pi A B) f (\(x:A) -> f x)) * unit

Функциональная экстенсиональность

В качестве бонус трека, funext. В этом примере мы показываем, что терм funext — это все-лишь интро правило, формация же есть классические изоморфизм двух функций f и g, которые находятся в пространстве функций A -> B (в этом примере не зависимых, зависимые вам на домашку).


 funext_form (A B: U) (f g: A -> B)
   : U = Path (A -> B) f g
 funext (A B: U) (f g: A -> B) (p: (x:A) -> Path B (f x) (g x))
   : funext_form A B f g
 happly (A B: U) (f g: A -> B) (p: funext_form A B f g) (x: A)
   : Path B (f x) (g x)
 funext_Beta (A B: U) (f g: A -> B) (p: (x:A) -> Path B (f x) (g x))
   : (x:A) -> Path B (f x) (g x)
 funext_Eta (A B: U) (f g: A -> B) (p: Path (A -> B) f g)
   : Path (Path (A -> B) f g) (funext A B f g (happly A B f g p)) p

Еще в качестве упражнения функциональную экстенсиональность можно выразить через интервал.


 data I = i0 | i1 | seg <i> [(i=0) -> i0, (i=1) -> i1]

В статье только сигнатуры, все пруфы в https://github.com/groupoid/cubical.